module checkCache [Addr, Data]
open cacheMemory [Addr, Data] as cache
open abstractMemory [Addr, Data] as amemory

fun alpha (c: CacheSystem): Memory {
	{m: Memory | m.data = c.main ++ c.cache}
	}

-- introduction of m, m' ensures that they exist, and gives witnesses if counterexample
assert ReadOK {
	all c: CacheSystem, a: Addr, d: Data, m: Memory |
		cache/read (c, a, d) and m = alpha (c) => amemory/read (m, a, d)
	}
check ReadOK

assert WriteOK {
	all c, c': CacheSystem, a: Addr, d: Data, m, m': Memory |
		cache/write (c, c', a, d) and m = alpha (c) and m' = alpha (c')
 			=> amemory/write (m, m', a, d)
	}
check WriteOK

assert LoadOK {
	all c, c': CacheSystem, m, m': Memory |
		cache/load (c, c') and m = alpha (c) and m' = alpha (c') => m = m'
	}
check LoadOK

assert FlushOK {
	all c, c': CacheSystem, m, m': Memory |
		cache/flush (c, c') and m = alpha (c) and m' = alpha (c') => m = m'
	}
check FlushOK

/* predicates for checking consistency of abstraction function, etc */
pred alpha_play (c: CacheSystem, m: Memory) {
	m = alpha (c)
	some c.cache and some c.main
	}
run alpha_play